Nuprl Lemma : predicate_implies_weakening 11,40
T:Type, P1, P2:(T). P1  P2  P1  P2 
latex

Definitionst  T, Type, x:AB(x), P  Q, f(a), P  Q, P  Q, P & Q, x:A. B(x), , P1  P2, P1  P2

origin